Nuprl Lemma : firstn_map
0,22
postcript
pdf
f
:(Top
Top),
n
:
,
l
:Top List. firstn(
n
;map(
f
;
l
)) ~ map(
f
;firstn(
n
;
l
))
latex
Definitions
Unit
,
P
Q
,
P
&
Q
,
P
Q
,
T
,
i
<
j
,
,
i
j
,
b
,
b
,
True
,
Prop
,
map(
f
;
as
)
,
A
B
,
A
,
False
,
i
j
,
P
Q
,
Top
,
x
:
A
.
B
(
x
)
,
t
T
,
Lemmas
nat
wf
,
top
wf
,
nat
properties
,
ge
wf
,
map
wf
,
first0
,
bnot
wf
,
assert
wf
,
le
wf
,
le
int
wf
,
bool
wf
,
lt
int
wf
,
assert
of
le
int
,
bnot
of
lt
int
,
true
wf
,
squash
wf
,
eqff
to
assert
,
iff
transitivity
,
assert
of
lt
int
,
eqtt
to
assert
origin